/-
Copyright (c) 2023 Junyan Xu. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Junyan Xu
-/

import linear_algebra.free_module.ideal_quotient
import ring_theory.norm

/-!
# Norms on free modules over principal ideal domains

> THIS FILE IS SYNCHRONIZED WITH MATHLIB4.
> Any changes to this file require a corresponding PR to mathlib4.
-/

open ideal polynomial

open_locale big_operators polynomial

variables {R S ι : Type*} [comm_ring R] [is_domain R] [is_principal_ideal_ring R] [comm_ring S]
  [is_domain S] [algebra R S]

section comm_ring

variables (F : Type*) [comm_ring F] [algebra F R] [algebra F S] [is_scalar_tower F R S]

/-- For a nonzero element `f` in an algebra `S` over a principal ideal domain `R` that is finite and
free as an `R`-module, the norm of `f` relative to `R` is associated to the product of the Smith
coefficients of the ideal generated by `f`. -/
lemma associated_norm_prod_smith [fintype ι] (b : basis ι R S) {f : S} (hf : f ≠ 0) :
  associated (algebra.norm R f) (∏ i, smith_coeffs b _ (span_singleton_eq_bot.not.2 hf) i) :=
begin
  have hI := span_singleton_eq_bot.not.2 hf,
  let b' := ring_basis b (span {f}) hI,
  classical,
  rw [← matrix.det_diagonal, ← linear_map.det_to_lin b'],
  let e := (b'.equiv ((span {f}).self_basis b hI) $ equiv.refl _).trans
    ((linear_equiv.coord S S f hf).restrict_scalars R),
  refine (linear_map.associated_det_of_eq_comp e _ _ _).symm,
  dsimp only [e, linear_equiv.trans_apply],
  simp_rw [← linear_equiv.coe_to_linear_map, ← linear_map.comp_apply, ← linear_map.ext_iff],
  refine b'.ext (λ i, _),
  simp_rw [linear_map.comp_apply, linear_equiv.coe_to_linear_map, matrix.to_lin_apply,
    basis.repr_self, finsupp.single_eq_pi_single, matrix.diagonal_mul_vec_single, pi.single_apply,
    ite_smul, zero_smul, finset.sum_ite_eq', mul_one, if_pos (finset.mem_univ _), b'.equiv_apply],
  change _ = f * _,
  rw [mul_comm, ← smul_eq_mul, linear_equiv.restrict_scalars_apply, linear_equiv.coord_apply_smul,
    ideal.self_basis_def],
  refl
end

end comm_ring

section field

variables {F : Type*} [field F] [algebra F[X] S] [finite ι]

instance (b : basis ι F[X] S) {I : ideal S} (hI : I ≠ ⊥) (i : ι) :
  finite_dimensional F (F[X] ⧸ span ({I.smith_coeffs b hI i} : set F[X])) :=
(adjoin_root.power_basis $ I.smith_coeffs_ne_zero b hI i).finite_dimensional

/-- For a nonzero element `f` in a `F[X]`-module `S`, the dimension of $S/\langle f \rangle$ as an
`F`-vector space is the degree of the norm of `f` relative to `F[X]`. -/
lemma finrank_quotient_span_eq_nat_degree_norm [algebra F S] [is_scalar_tower F F[X] S]
  (b : basis ι F[X] S) {f : S} (hf : f ≠ 0) :
  finite_dimensional.finrank F (S ⧸ span ({f} : set S)) = (algebra.norm F[X] f).nat_degree :=
begin
  haveI := fintype.of_finite ι,
  have h := span_singleton_eq_bot.not.2 hf,
  rw [nat_degree_eq_of_degree_eq (degree_eq_degree_of_associated $ associated_norm_prod_smith b hf),
      nat_degree_prod _ _ (λ i _, smith_coeffs_ne_zero b _ h i), finrank_quotient_eq_sum F h b],
  -- finrank_quotient_eq_sum slow
  congr' with i,
  exact (adjoin_root.power_basis $ smith_coeffs_ne_zero b _ h i).finrank
end

end field
